The system contains multiple components, e.g., the users, the lifts, the floors, the internal button panels, etc. There are non-trivial data components and data operations, e.g., the internal requests and external requests and the operations to add/delete requests. For simplicity, we assume there is no central controller for assigning external requests. Instead, each lift functions on its own to find and serve requests, in the following way. Initially, a lift resides at the ground level ready to travel upwards. Whenever there is a request (from the internal button panel or outside button) for the current residing floor, the lift opens the door and later closes it. Otherwise, if
there are requests for a floor on the current traveling direction (e.g., a request for floor 3 when the lift is at floor 1 traveling upwards), then the lift keeps traveling on the current direction. Otherwise, the lift changes its direction. Other constraints on the system include that a user may only enter a lift when the door is open, there could be an internal request if and only if there is a user inside, etc.

Shared variables offer an alternative means of communication among processes (which reside at the same computing device or are
connected by wires with negligible transmission delay). They record the global state and make the information available to all processes. In the lift example, the internal/external requests can be naturally modeled as shared arrays. In CSP#, they are declared as follows.

• #define NoOfFloor 3;
• #define NoOfLift 2;
• var extUpReq[NoOfFloor];
• var extDownReq[NoOfFloor];
• var intRequests[NoOfLift][NoOfFloor];
• var doorOpen[NoOfLift];

Where "define" and "var" are reserved keywords. The former defines a global constant, e.g., "NoOfFloor" which denotes the number of floors and "NoOfLift" which denotes the number of lifts. The latter defines a variable, e.g., "extUpReq" and "extDownReq" which store external requests, "intRequests" which store internal requests and "doorOpen" which captures lift doors' states. CSP# has a weak type system (like JSP) and therefore type information is not necessary for variable declaration. By default, all the above defined are treated as arrays of integers. In particular, elements in "extUpReq" (or "extDownReq") are binary: 1 at j-th position means that there is a request for traveling upwards (or downwards) at j-th floor; 0 means no request. Two dimensional array "intRequests" stores internal requests from all lifts. In particular, the internal request for the j-th floor from the i-th lift is stored at "intRequests[i][j]" in the array. Elements in "intRequests" are binary: 1 means that the floor has been requested and 0 means not requested. Elements in array "doorOpen" range from -1 to "NoOfFloor-1". The i-th element of "doorOpen" is -1 if and only if the door of i-th lift is closed, otherwise it is j such that j >= 0 if and only if the i-th lift has opened door at j-th floor. We assume that initially all doors are closed. We remark if the Z language is used for specification, specific types for elements in the arrays may be defined to constrain their values. In CSP#, we instead use PAT to verify that the constraints hold given any system behavior.

Associated with the variables are data operations which query or modify the variables. In the lift system, whenever a lift opens its door, the requests must be updated accordingly. For instance, the codes shown below clear the requests when the i-th lift opens the door at level-th floor. Let dir be the current traveling direction (1 for upwards and -1 for downwards). The first line clears internal requests, by simply resetting the respective position in array "intRequests" to 0. The rest clears external requests. Only the request along the lift's traveling direction is cleared.

• intRequests[i][level] = 0;
• if (dir > 0) {
•         extUpReq[level] = 0;
• }
• else {
•         extDownReq[level] = 0;
• }

A more complicated operation is to determine whether there are requests along the current traveling direction, so as to determine whether a lift should keep traveling in the same direction or to change direction. This operation may be implemented by the codes below, where "level" is a variable recording the floor that the lift is residing at, "index" is a loop counter and "result[i]" records the result (0 for no such request and 1 for
yes). A while-loop is used to search for a request along the current traveling direction, e.g., if the lift is traveling upwards, we search for a request for (or from) an upper floor. The search starts with the next floor "level+dir" and stops when the ground or top floor is reached.

A system may contain multiple data operations, each of which is terminating and is assumed to be executed atomically. They can be implemented using the CSP# syntax as shown above, or they can be implemented using existing programming languages. For instance, we offer the keyword call in PAT to allow invocation of data operations (as atomic events) implemented externally as C# static methods in CSP# models. Data operations may be invoked alternatively or in parallel. In CSP#, data operations can be treated as atomic events and composed using compositional operators. From another point of view, we allow an event to be associated with an optional sequential terminating program. For instance, the program above may be labeled as event "checkIfToMove.i.level", which then can be used to constitute CSP process expressions, e.g., refer to later discussion. Data races are prevented by not allowing synchronization of events containing procedural code.

• index = level+dir;
• result[i] = 0;
• while (index >= 0 && index < NoOfFloor && result[i] == 0) { 
•              if (extUpReq[index] != 0 || extDownReq[index] != 0 || intRequests[i][index] != 0) {
•                          result[i] = 1;
•              }
•             else {
•                          index=index+dir;
•             }
• }

The high-level compositional operators in CSP capture common system behavior patterns. They are very useful in system modeling. Furthermore, process equivalence can be proved or disproved by appealing to algebraic laws which are defined for the operators. In CSP#, we reuse most of the operators and integrate them with our extensions in a rigorous way so as to maximally preserve the algebraic laws.

In CSP#, we support global variables which are globally accessible, process parameters which are accessible in the respective process expression and local variables which are accessible in one data operation. We restrict the use of local variables in general. In particular, local variables introduced as process parameters or variables to store channel inputs cannot be modified by event associated programs. They can, however, be modified indirectly.

The following is a process "Lift" which concisely models the behavior of one lift.

• Lift(i, level, dir) =
•     if ((dir > 0 && extUpReq[level] == 1) || (dir < 0 && extDownReq[level] == 1) || intRequests[i][level] == dir) {
•         opendoor.i {
•                 doorOpen[i] = level;
•                 intRequests[i][level] = 0;
•                 if (dir > 0) {
•                         extUpReq[level] = 0;
•                 }
•                 else {
•                         extDownReq[level] = 0;
•                 }
•         } ->
•         closedoor.i{doorOpen[i] = -1} -> Lift(i,level, dir)
•     }
•     else {
•         checkIfToMove.i.level{
•                 index = level+dir;
•                 result[i] = 0;
•                 while (index >= 0 && index < NoOfFloor && result[i] == 0) { 
•                          if (extUpReq[index] != 0 || extDownReq[index] != 0 || intRequests[i][index] != 0) {
•                                  result[i] = 1;
•                          }
•                         else {
•                                 index=index+dir;
•                         }
•                 }
•         } ->
•         if (result[i] == 1) {
•                 moving.i.dir ->
•                 if (level+dir == 0 || level+dir == NoOfFloors-1) {
•                         Lift(i, level+dir, -1*dir)
•                 }
•                 else {
•                         Lift(i, level+dir, dir)
•                 }
•         }
•         else {
•                 if ((level == 0 && dir == 1) || (level == NoOfFloors-1 && dir == -1)) {
•                         Lift(i, level, dir)
•                 }
•                 else {
•                         changedir.i.level -> Lift(i, level, -1*dir)
•                 }
•         }
• };

Notice that the process has multiple parameters, namely "i" which is an identifier of the lift, "level" which denotes the residing floor and $dir$ which denotes the current traveling direction (1 for traveling upwards and -1 for downwards). The condition at line 7 is used to check whether there is a request for the current floor, with the correct traveling direction if it is external. If yes, then the door is opened, the requests for the floor are cleared (using the code presented above), and then the door is closed. Otherwise, the lift checks whether to continue traveling on the same direction (using the code presented above). If the result is 1, then the lift moves to the next floor. Otherwise, the lift changes its direction and then repeats from the start. In this example, we have events which are associated with programs and simple events like "moving.i.dir". The rest of the system model is presented below.

• var  index; 
• var result[NoOfLift];
• Users() = ||| x:{0..2} @ aUser();
• aUser() = [] pos:{0..NoOfFloor-1} @ (ExternalPush(pos); Waiting(pos));
• ExternalPush(pos) = case {
•         pos == 0 : pushup.pos{extUpReq[pos] = 1} -> Skip
•         pos == NoOfFloor-1 : pushdown.pos{extDownReq[pos] = 1} -> Skip
•         default : pushup.pos{extUpReq[pos] = 1} -> Skip [] pushdown.pos{extDownReq[pos] = 1} -> Skip
• };
• Waiting(pos) = [] i:{0..NoOfLift-1} @ ([doorOpen[i] == pos]enter.i -> []x:{0..NoOfFloor-1} @ (push.x{intRequests[i][x] = 1} -> [doorOpen[i] == x]exit.i.x -> User()));
• LiftSystem() = Users() ||| (||| x:{0..NoOfLift-1} @ Lift(x, 0, 1));

The first two lines define the rest of the variables. Then we model users' behavior in the lift system. The behavior of three users is defined as the interleaving of each user, where "||| x:{i..j} @ P(x)" is equivalent to "P(i) ||| ... ||| P(j)". Behavior of a user is specified as process "aUser". Each user may initially be at any floor. This is captured using indexed external choice. The user pushes a button (for traveling upwards or downwards, specified as "ExternalPush(pos)") and then waits for the lift to come (specified as "Waiting(pos)").

A "case" statement, which is a syntactic sugar for multiple if-then-else statements, is used in process "ExternalPush(pos)". We remark that the conditions in the case statement are evaluated in the order until one which evaluates to be true is found. Otherwise, the "default" branch is taken. In the example, if the user is at the ground floor or the top one, only one direction to travel can be requested. Otherwise, the user may choose either to go upwards or downwards. Lines 5 to 7 capture how the external requests are updated.

The user then waits until a lift opened its door at the user's floor (captured by condition "doorOpen[i] == pos") and then enters the lift. We remark that this model allows users to enter the lift with the wrong traveling direction (which may happen in real world). After making an internal request, the user may exit when the door is opened again at his/her destination floor. The lift system is modeled as the interleaving of users and multiple lifts. Initially, the lifts are residing at the ground floor, ready to travel upwards. In this example, we demonstrate how variable updates and compositional operators may be used together seamlessly to capture system behavior.

Once we have a model, we may use PAT to simulate its behaviors. Alternatively, we may write assertions about critical system properties and invoke the PAT model checkers to examine the model in order to find counterexamples, as follows.

• #assert LiftSystem() deadlockfree;
• #define pr1 extUpReq[0] > 0;
• #define pr2 extUpReq[0] == 0;
• #assert LiftSystem() |= [] (pr1 -> <> pr2) && [] <> moving.0